open import Relation.Unary using ( Pred ; U; Decidable )
open import Algebra.Structures using (  IsGroup ; IsAbelianGroup ; IsSemigroup)
open import Algebra using ( Group ; Monoid ; Semigroup ; AbelianGroup)
open import Relation.Binary using ( Rel )
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Level using ( Level ; _⊔_ ; suc )
open import Data.Product using ( _×_ ; _,′_ ) 
import Relation.Binary.HeterogeneousEquality.Quotients
open import Data.Product using (_,_)
open import Data.Product using (proj₁ ; proj₂ )

open import Relation.Binary.Core using (IsEquivalence ; _Respects_ ; _Respects₂_ )
open import Relation.Binary
open import Algebra.Structures
open import Substructures using (IsNormalSubGroup ; NormalSubGroup )
open import QuotientRelation using (QuotientRelation ; quotientGroupIsAGroup)
open import Kern using (Kernₕ)

open import Algebra.Morphism using ( IsGroupMorphism )

module II-1-1 where

--{a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (isInSubset : Pred A b) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A)
--  (isGroup : IsGroup _≈_ _∙_ ε _⁻¹) (isNormalSubGroup : IsNormalSubGroup _≈_ isInSubset _∙_ ε _⁻¹) where

-- f is  homm G/N to L
th1-1 : ∀ {a₁ ℓ₁ a₂ ℓ₂ b} (h : Group a₁ ℓ₁) (l : Group a₂ ℓ₂) → let open Group in
  (N : Pred (h. Carrier) b) → 
  (isN : IsNormalSubGroup (h. _≈_)  N (h. _∙_) (h. ε) (h. _⁻¹)) (fn : (h. Carrier) → (l. Carrier)) →
  (fnP : (a : (h. Carrier)) → (N a) → ((l. _≈_) (fn a)) (l. ε)  )
  (isHomm : IsGroupMorphism h l fn  )  →
  let 
   ≈ₙ = (QuotientRelation (h. Carrier) N (h.  _∙_) (h. _⁻¹)) 
   isGroupH\N = quotientGroupIsAGroup h N isN
   h\n : Group a₁ b
   h\n = record { Carrier = (h. Carrier) ; _≈_ = ≈ₙ ; _∙_ = (h. _∙_) ; ε = h. ε ; _⁻¹ = h. _⁻¹ ; isGroup = isGroupH\N }
  in
   (IsGroupMorphism h\n l fn)
th1-1
  h@record { Carrier = Carrierₕ ; _≈_ = _≈ₕ_ ; _∙_ = _∙ₕ_ ; ε = εₕ ; _⁻¹ = _⁻¹ₕ ; isGroup = isGroupₕ }
  l@record { Carrier = Carrierₗ ; _≈_ = _≈ₗ_ ; _∙_ = _∙ₗ_ ; ε = εₗ ; _⁻¹ = _⁻¹ₗ ; isGroup = isGroupₗ }
  N isN fn fnP isHomm = let open Group in let
  _≈ₙ_ = (QuotientRelation Carrierₕ N _∙ₕ_ _⁻¹ₕ) 
  isGroupH\N = quotientGroupIsAGroup h N isN
  proof : (a b : Carrierₕ) → (a ≈ₙ b) → ((fn a) ≈ₗ (fn b)) 
  proof a b a≈ₙb = let
    dd1 : fn (a ∙ₕ (b ⁻¹ₕ)) ≈ₗ εₗ
    dd1 = fnP _ a≈ₙb
    dd1' : fn (a ∙ₕ (b ⁻¹ₕ)) ≈ₗ (fn εₕ)
    dd1' = (trans l) dd1  ((sym l) (IsGroupMorphism.ε-homo isHomm))
    dd1'' : (fn b ⁻¹ₗ) ≈ₗ fn (b ⁻¹ₕ)
    dd1'' = ((l. sym) ((IsGroupMorphism.⁻¹-homo) isHomm b))
    dd2 : fn (a ∙ₕ (b ⁻¹ₕ)) ≈ₗ (fn a ∙ₗ fn (b ⁻¹ₕ))
    dd2 =  (IsGroupMorphism.∙-homo isHomm) a (b ⁻¹ₕ)
    dd3 : (fn a ∙ₗ fn (b ⁻¹ₕ)) ≈ₗ εₗ 
    dd3 = (trans l) ((sym l) dd2) dd1
    dd4 : ((fn a ∙ₗ fn (b ⁻¹ₕ)) ∙ₗ (fn b)) ≈ₗ  (εₗ ∙ₗ (fn b))
    dd4 = (l. ∙-cong)  dd3 (l. refl)
    transₗ = l. trans
    assoc = l. assoc
    qq1 : ((fn a ∙ₗ fn (b ⁻¹ₕ)) ∙ₗ fn b) ≈ₗ (fn a ∙ₗ (fn (b ⁻¹ₕ) ∙ₗ fn b))
    qq1 = assoc (fn a) (fn (b ⁻¹ₕ)) (fn b)
    qqxD : (fn a ∙ₗ (((fn b) ⁻¹ₗ) ∙ₗ fn b)) ≈ₗ (fn a)
    qqxD = transₗ  ((l. ∙-cong) ((l. refl) {fn a}) (proj₁ (l. inverse) (fn (b)))) (proj₂ (l. identity) (fn a))
    ddd : (fn (b ⁻¹ₕ)) ≈ₗ ((fn b)  ⁻¹ₗ)
    ddd = (IsGroupMorphism.⁻¹-homo) isHomm b 
    symₗ = l. sym
    reflₗ = l. refl
    ∙-congₗ = l. ∙-cong
    ddd2 : (fn a ∙ₗ (((fn b) ⁻¹ₗ) ∙ₗ fn b)) ≈ₗ (fn a ∙ₗ (fn (b ⁻¹ₕ) ∙ₗ fn b))
    ddd2 = ∙-congₗ  reflₗ (∙-congₗ (symₗ ddd) (reflₗ {fn b}))
    qq2 : (fn a ∙ₗ (fn (b ⁻¹ₕ) ∙ₗ fn b)) ≈ₗ (fn a)
    qq2 =  transₗ ((l. sym) ddd2) qqxD  
    in transₗ ((l. sym) (transₗ qq1 qq2)) (transₗ dd4 (proj₁ (l. identity) (fn b)))
  in let open IsGroupMorphism in
    record { mn-homo = record {sm-homo = record {⟦⟧-cong = λ {a} {b} a≈ₙb → proof a b a≈ₙb ; ∙-homo = IsGroupMorphism.∙-homo isHomm} ;  ε-homo = IsGroupMorphism.ε-homo isHomm} }


{-- (onto to surjekcja)
teraz dodatkowe tw:
if f is onto and the kernel of f is N then f is an isomorphism from H\N toL

 is a homomorphism or morphism (i.e. a mathematical mapping) that can be reversed by an inverse morphism
--}

open import Function.Surjection
open import Function.Inverse
open import Function.Bijection
open import Function.Equality using (_⟶_ ; Π)

open import Data.Product
--wikipedia
-- iven two groups (G, ∗) and (H, ⊙ {\displaystyle \odot } \odot ), a group isomorphism from (G, ∗) to (H, ⊙ {\displaystyle \odot } \odot ) is a bijective group homomorphism from G to H. Spelled out, this means that a group isomorphism is a bijective function f : G → H {\displaystyle f:G\rightarrow H} f:G\rightarrow H such that for all u and v in G it holds that 
--import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
th1-1′ : ∀ {a₁ ℓ₁ a₂ ℓ₂ } (h : Group a₁ ℓ₁) (l : Group a₂ ℓ₂) → let open Group in
  (fn : (h. Carrier) → (l. Carrier)) →
  (isHomm : IsGroupMorphism h l fn  )  →
  let
    kern = Kernₕ isHomm --kern zamiast N z poprzedniego tw.
    hₛ = setoid h
    lₛ = setoid l
    fnₕₗ : (hₛ ⟶ lₛ)
    fnₕₗ = record { _⟨$⟩_ = fn ; cong = IsGroupMorphism.⟦⟧-cong isHomm}
  in
  (surf : Surjective {From = hₛ} {To = lₛ} fnₕₗ)
  (isN : IsNormalSubGroup (h. _≈_) kern (h. _∙_) (h. ε) (h. _⁻¹)) → 
  let 
   ≈ₙ = (QuotientRelation (h. Carrier) kern (h.  _∙_) (h. _⁻¹)) 
   isGroupH\N = quotientGroupIsAGroup h kern isN
   h\n : Group a₁ ℓ₂
   h\n = record { Carrier = (h. Carrier) ; _≈_ = ≈ₙ ; _∙_ = (h. _∙_) ; ε = h. ε ; _⁻¹ = h. _⁻¹ ; isGroup = isGroupH\N }
   h\nHomm : (IsGroupMorphism h\n l fn)
   h\nHomm = th1-1 h l kern isN fn (λ _ x → x) isHomm
   h\nₛ = setoid h\n
   fnₕₙₗ : (h\nₛ ⟶ lₛ) 
   fnₕₙₗ = record { _⟨$⟩_ = fn ; cong = IsGroupMorphism.⟦⟧-cong h\nHomm}
  in
  --f jest izomorfizmem, czyli: f jest biekcją i f⁻¹ jest homomorfizmem
  Σ (Bijective fnₕₙₗ)  λ b → IsGroupMorphism l h\n (λ (x : (l. Carrier)) → Bijective.from b Π.⟨$⟩ x)
th1-1′ {a₁} {ℓ₁} {a₂} {ℓ₂}
  h@record { Carrier = Carrierₕ ; _≈_ = _≈ₕ_ ; _∙_ = _∙ₕ_ ; ε = εₕ ; _⁻¹ = _⁻¹ₕ ; isGroup = isGroupₕ }
  l@record { Carrier = Carrierₗ ; _≈_ = _≈ₗ_ ; _∙_ = _∙ₗ_ ; ε = εₗ ; _⁻¹ = _⁻¹ₗ ; isGroup = isGroupₗ }
  fn isHomm surf isN = let
   kern = Kernₕ isHomm
   hₛ = Group.setoid h
   lₛ = Group.setoid l
   fnₕₗ : (hₛ ⟶ lₛ)
   fnₕₗ = record { _⟨$⟩_ = fn ; cong = IsGroupMorphism.⟦⟧-cong isHomm}
   _≈ₙ_ = (QuotientRelation Carrierₕ kern  _∙ₕ_  _⁻¹ₕ) 
   isGroupH\N = quotientGroupIsAGroup h kern isN
   h\n : Group a₁ ℓ₂
   h\n = record { Carrier = Carrierₕ ; _≈_ = _≈ₙ_ ; _∙_ =  _∙ₕ_ ; ε = εₕ ; _⁻¹ = _⁻¹ₕ ; isGroup = isGroupH\N }
   h\nHomm : (IsGroupMorphism h\n l fn)
   h\nHomm = th1-1 h l kern isN fn (λ _ x → x) isHomm
   h\nₛ = Group.setoid h\n
   fnₕₙₗ : (h\nₛ ⟶ lₛ)
   fnₕₙₗ = record { _⟨$⟩_ = fn ; cong = IsGroupMorphism.⟦⟧-cong h\nHomm}

--if F(a) = F(b), then F(ab-1 ) = 1, so ab- 1 ∈ N and a = b (mod N). Therefore F is a one-to-one map from G/N to L
   injectiveQ : (x : Carrierₕ) (y : Carrierₕ) (x≈ₗy : fn x ≈ₗ fn y) →  (x ≈ₙ y)
   injectiveQ = λ x y x≈ₗy → let
     eq1 : (fn x ∙ₗ (fn y ⁻¹ₗ)) ≈ₗ (fn y ∙ₗ (fn y ⁻¹ₗ))
     eq1 = (Group.∙-cong l) x≈ₗy (Group.refl l {(fn y) ⁻¹ₗ})
     eq2 :  (fn y ∙ₗ (fn y ⁻¹ₗ)) ≈ₗ εₗ
     eq2 = proj₂ (Group.inverse l) (fn y)   
     tq1 : (fn (x ∙ₕ (y ⁻¹ₕ))) ≈ₗ (fn x ∙ₗ fn (y ⁻¹ₕ))
     tq1 = IsGroupMorphism.∙-homo h\nHomm x (y ⁻¹ₕ)
     end : fn (y ⁻¹ₕ) ≈ₗ (fn y ⁻¹ₗ)
     end = IsGroupMorphism.⁻¹-homo isHomm y 
     in
       (Group.trans l) (Group.trans l (Group.trans l tq1 ((Group.∙-cong l) (Group.refl l {fn x}) end)) eq1)  eq2 

   fn⁻¹ : Carrierₗ → Carrierₕ
   fn⁻¹ = λ x → Surjective.from surf Π.⟨$⟩ x 
   congQ2 : (x : Carrierₗ) → (y : Carrierₗ) → (x ≈ₗ y) → (fn ((fn⁻¹ x) ∙ₕ ((fn⁻¹ y) ⁻¹ₕ))) ≈ₗ εₗ
   congQ2 x y x≈ₗy = let
     qq1 : (x ∙ₗ (y ⁻¹ₗ)) ≈ₗ εₗ
     qq1 = (Group.trans l) (Group.∙-cong l x≈ₗy (Group.refl l {(y ⁻¹ₗ)})) (Group.inverseʳ l y)

     qe0 : (fn εₕ) ≈ₗ εₗ
     qe0 = IsGroupMorphism.ε-homo isHomm
     qee1 : (fn (fn⁻¹ εₗ)) ≈ₗ εₗ
     qee1 = ((Surjective.right-inverse-of surf) εₗ)
     qee2 : (fn (fn⁻¹ εₗ)) ≈ₗ (fn εₕ)
     qee2 = (Group.trans l) qee1 ((Group.sym l) qe0)

    -- qe1 : (fn⁻¹ εₗ) ≈ₕ εₕ
     --qe1 = {!((Surjective.right-inverse-of surf) (fn εₕ))!}
     qq2pre1 : (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ))) ≈ₕ (fn⁻¹ εₗ)
     qq2pre1 = Π.cong (Surjective.from surf) qq1 
     --qq2 : (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ))) ≈ₕ εₕ
     --qq2 = (Group.trans h) qq2pre1 qe1

     fn⁻¹-cong = Π.cong (Surjective.from surf)
     --qw1 : ((fn⁻¹ x) ∙ₕ (fn⁻¹ (y ⁻¹ₗ))) ≈ₕ (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ)))
     --qw1 = {!!}
     --qw101 : ((fn⁻¹ y) ⁻¹ₕ) ≈ₕ (fn⁻¹ (y ⁻¹ₗ))
     --qw101 = {!!}
     --noToJedziemy : ((fn⁻¹ x) ∙ₕ ((fn⁻¹ y) ⁻¹ₕ)) ≈ₕ (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ)))
     --noToJedziemy = Group.trans h (Group.∙-cong h (Group.refl h {(fn⁻¹ x)}) qw101) qw1

     $$$ = fn ((fn⁻¹ (x ∙ₗ (y ⁻¹ₗ))) ⁻¹ₕ) ≈ₗ (fn (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ))) ⁻¹ₗ)
     $$$  = IsGroupMorphism.⁻¹-homo isHomm  (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ)))

     elo1 : fn (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ))) ≈ₗ (x ∙ₗ (y ⁻¹ₗ))
     elo1 = ((Surjective.right-inverse-of surf) (x ∙ₗ (y ⁻¹ₗ)))
     elo2 : fn ((fn⁻¹ x) ∙ₕ ((fn⁻¹ y) ⁻¹ₕ)) ≈ₗ ((fn (fn⁻¹ x)) ∙ₗ ((fn ((fn⁻¹ y) ⁻¹ₕ))))
     elo2 =  IsGroupMorphism.∙-homo isHomm (fn⁻¹ x) ((fn⁻¹ y) ⁻¹ₕ)

     chodźNaPole : fn ((fn⁻¹ y) ⁻¹ₕ) ≈ₗ ((fn (fn⁻¹ y)) ⁻¹ₗ)
     chodźNaPole = IsGroupMorphism.⁻¹-homo isHomm (fn⁻¹ y)
     l3ll3 : (fn (fn⁻¹ y)) ≈ₗ y
     l3ll3 = Surjective.right-inverse-of surf y -- to jest ostatni skończony wiersz :D :D :D:D::DDDDDDDDD
     krakowskiRapKontratakuje : ((fn (fn⁻¹ y)) ⁻¹ₗ) ≈ₗ (y ⁻¹ₗ)
     krakowskiRapKontratakuje = Group.⁻¹-cong l  l3ll3
     iCoZTym : fn ((fn⁻¹ y) ⁻¹ₕ) ≈ₗ (y ⁻¹ₗ)
     iCoZTym = Group.trans l chodźNaPole krakowskiRapKontratakuje
     cel-1 : (fn (fn⁻¹ x) ∙ₗ fn ((fn⁻¹ y) ⁻¹ₕ)) ≈ₗ (x ∙ₗ (y ⁻¹ₗ))
     cel-1 = (Group.∙-cong l) (Surjective.right-inverse-of surf x) iCoZTym
     cel : (fn ((fn⁻¹ x) ∙ₕ ((fn⁻¹ y) ⁻¹ₕ))) ≈ₗ fn (fn⁻¹ (x ∙ₗ (y ⁻¹ₗ)))
     cel = (Group.trans l) (Group.trans l elo2 cel-1) (Group.sym l elo1) 
     in (Group.trans l) (Group.trans l cel (Π.cong fnₕₗ qq2pre1)) qee1
   congQ : (x : Carrierₗ) → (y : Carrierₗ) → (x ≈ₗ y) → Kernₕ isHomm ((Surjective.from surf Π.⟨$⟩ x) ∙ₕ ((Surjective.from surf Π.⟨$⟩ y) ⁻¹ₕ))
   congQ = congQ2

   fnₕₙₗ⁻¹ : (lₛ ⟶ h\nₛ) 
   fnₕₙₗ⁻¹ =  record { _⟨$⟩_ = fn⁻¹ ; cong = λ {x} {y} eq → congQ x y eq}

   right-inverse-ofQ : (x : Carrierₗ) → ((fn (fn⁻¹ x)) ≈ₗ x)
   right-inverse-ofQ = Surjective.right-inverse-of surf
   surjectiveQ : Surjective fnₕₙₗ
   surjectiveQ = record { from = fnₕₙₗ⁻¹; right-inverse-of =  right-inverse-ofQ }

   --x : Carrierₗ → (Surjective.from (Bijective.surjective b) Π.⟨$⟩ x)
   bijection = record { injective = λ {x} {y} x≈ₗy → injectiveQ x y x≈ₗy ; surjective = surjectiveQ }
   ε-homoQ : fn ( fn⁻¹ εₗ  ∙ₕ (εₕ ⁻¹ₕ)) ≈ₗ εₗ 
   ε-homoQ = let
     q : (fn ( fn⁻¹ εₗ  ∙ₕ (εₕ ⁻¹ₕ))) ≈ₗ ((fn (fn⁻¹ εₗ)) ∙ₗ (fn (εₕ ⁻¹ₕ)))
     q = IsGroupMorphism.∙-homo isHomm (fn⁻¹ εₗ) (εₕ ⁻¹ₕ)
     toJużByło : (fn (fn⁻¹ εₗ)) ≈ₗ εₗ
     toJużByło = Surjective.right-inverse-of surjectiveQ _
     eee : (εₕ ⁻¹ₕ) ≈ₕ εₕ
     eee = (Group.trans h) (Group.sym h (Group.identityˡ h (εₕ ⁻¹ₕ))) (Group.inverseʳ h εₕ)
     e2 : (fn (εₕ ⁻¹ₕ)) ≈ₗ (fn  εₕ)
     e2 = IsGroupMorphism.⟦⟧-cong isHomm eee
     in Group.trans l q (Group.trans l (Group.∙-cong l toJużByło (Group.trans l e2 (IsGroupMorphism.ε-homo isHomm)))  (Group.identityˡ l εₗ))
   ∙-homoQ : (x : Carrierₗ) → (y : Carrierₗ) →  fn ((fn⁻¹ (x ∙ₗ y)) ∙ₕ (((fn⁻¹ x) ∙ₕ (fn⁻¹ y)) ⁻¹ₕ))  ≈ₗ εₗ
   ∙-homoQ x y = let
     edd : fn ((fn⁻¹ (x ∙ₗ y)) ∙ₕ (((fn⁻¹ x) ∙ₕ (fn⁻¹ y)) ⁻¹ₕ)) ≈ₗ  ((fn ((fn⁻¹ (x ∙ₗ y)))) ∙ₗ (fn (((fn⁻¹ x) ∙ₕ (fn⁻¹ y)) ⁻¹ₕ)))
     edd = IsGroupMorphism.∙-homo isHomm _ _
     q0 : fn (fn⁻¹ (x ∙ₗ y)) ≈ₗ (x ∙ₗ y)
     q0 = right-inverse-ofQ  (x ∙ₗ y)
     
     ddd :  fn ((fn⁻¹ x) ∙ₕ  (fn⁻¹ y)) ≈ₗ ((fn ((fn⁻¹ x))) ∙ₗ fn ((fn⁻¹ y)))
     ddd = (IsGroupMorphism.∙-homo isHomm  (fn⁻¹ x) (fn⁻¹ y))
     ostatni :  (fn (fn⁻¹ x) ∙ₗ  fn (fn⁻¹ y)) ≈ₗ (x ∙ₗ y)
     ostatni = Group.∙-cong l (right-inverse-ofQ x) (right-inverse-ofQ y)
     c1 : (fn (((fn⁻¹ x) ∙ₕ (fn⁻¹ y))  ⁻¹ₕ)) ≈ₗ (((x ∙ₗ y)) ⁻¹ₗ)
     c1 = Group.trans l (IsGroupMorphism.⁻¹-homo isHomm (((fn⁻¹ x) ∙ₕ (fn⁻¹ y)))) (Group.⁻¹-cong l (Group.trans l ddd ostatni))
     in  (Group.trans l edd (Group.trans l (Group.∙-cong l q0 c1) (Group.inverseʳ  l _)))
   in
   bijection , record { mn-homo = record { sm-homo = record { ⟦⟧-cong = λ {x} {y} eq → congQ x y eq ; ∙-homo = ∙-homoQ } ; ε-homo = ε-homoQ } }  
